FDL - Step of Proof: adjacent-nil

Step of Proof: adjacent-nil

Inference at *
Iof proof for Lemma adjacent-nil:

T:Type, x, y:T. adjacent(T;[];x;y)

False

by ((((Unfold `adjacent` 0)

CollapseTHEN (MaAuto

))

)

CollapseTHEN (((Reduce (-1))

CoCollapseTHEN (((ExRepD

)

CollapseTHEN (Auto

))

))

))

C.

Definitions adjacent(T;L;x;y), x:A. B(x), x:AB(x), (x l), n - m, ||as||, , l[i], n+m, #$n, [], t T, x:A. B(x), x:A B(x), s = t, Type, {i..j}, {x:A| B(x)} , , i j < k, A B, P & Q, A, False, P Q, Void, -n

Lemmas false wf, int seg wf